package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class ToyI1 {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("ToyI1");
		 
         // Variables
		 TypedData x = new TypedData("x", Constants.TYPE_INTEGER);
		 tiosts.addVariable(x);
         
         // There are no parameters       
         
         Action init3 = new Action("Init3", Constants.ACTION_INTERNAL);
         tiosts.addAction(init3);
         Action b = new Action("b", Constants.ACTION_INPUT);
         tiosts.addAction(b);
         tiosts.addActionParameter(x);
         Action aInput = new Action("a", Constants.ACTION_INPUT);
         tiosts.addAction(aInput);     
         Action aOutput = new Action("a", Constants.ACTION_OUTPUT);
         tiosts.addAction(aOutput); 
         
         Location start3 = new Location("Start3");
         tiosts.addLocation(start3);
         Location s6 = new Location("S6");
         tiosts.addLocation(s6);
         Location s7 = new Location("S7");
         tiosts.addLocation(s7);        
         Location s8 = new Location("S8");
         tiosts.addLocation(s8);
         Location s9 = new Location("S9");
         tiosts.addLocation(s9);
         Location lc3 = new Location("lc3");
         tiosts.addLocation(lc3);
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start3);
         
         // Transitions
         tiosts.createTransition("Start3", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init3, null, null, "S6");
         tiosts.createTransition("S6", Constants.GUARD_TRUE, Constants.GUARD_TRUE, b, "x := 0", null, "S7");
         tiosts.createTransition("S7", "x < 4", Constants.GUARD_TRUE, aOutput, null, null, "S8");
         tiosts.createTransition("S8", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aInput, null, null, "S9");
         tiosts.createTransition("S6", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aInput, null, null, "lc3");
         tiosts.createTransition("S7", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aInput, null, null, "lc3");
         tiosts.createTransition("S7", Constants.GUARD_TRUE, Constants.GUARD_TRUE, b, null, null, "lc3");
         tiosts.createTransition("S8", Constants.GUARD_TRUE, Constants.GUARD_TRUE, b, null, null, "lc3");
         tiosts.createTransition("S9", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aInput, null, null, "lc3");
         tiosts.createTransition("S9", Constants.GUARD_TRUE, Constants.GUARD_TRUE, b, null, null, "lc3");
         
         return tiosts;		 
	 }

}
